Upgrade Lean and dependencies to 4.34.1 - #4

Upgrade the branch from Lean 4.29.0-rc8 to Lean 4.34.1, with matching mathlib and doc-gen4 revisions. Pin the migrated polynomial and Gröbner dependencies to published commits so this branch can build before their PRs are merged:

• chore: upgrade to Lean 4.34.1 groebner_proj#8
• chore: upgrade to Lean 4.34.1 MonomialOrderedPolynomial#2

Adapt the renamed Gröbner-basis theorem and proof elaboration changes, remove an obsolete internal Lean import, and fix the out-of-scope set reference in submodule_span. Scope the legacy transparency behavior to tactic execution so callers can use gb_solve with default Lean options. Update the proof templates and remove two proof steps that simp now discharges. Give one rational-coefficient remainder example a local heartbeat budget of 800000 after verifying that its default-budget kernel timeout is resolved. No new sorry or axioms.

Validation:

• lake build GroebnerTac GroebnerTac.Lemma and lake build GroebnerTac.Template
• lake build groebner/Groebner
• lake build doc-gen4/doc-gen4 using the native C compiler
• Kernel-checked smoke proofs for zero/nonzero remainders, Gröbner bases, and ideal membership/nonmembership; axiom checks contain no sorryAx.
• Completed lake build GroebnerTac GroebnerTac.Example GroebnerTac.Template GroebnerTac.Lemma against the original source. All modules and examples passed except the explicit remote Sage API example at Example.lean:31, which failed because the external service's HTTPS connection ended with SSL: UNEXPECTED_EOF_WHILE_READING. The same mathematical example with local Sage is also present in the file and passed. No kernel timeouts remained.
• The PR's GitHub CI build and documentation workflow passed.
• GroebnerTac/Cyclic3.lean is intentionally excluded, as requested, and remains untouched and untracked.